Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	a__filter(cons(X,Y),0,M)	→ cons(0,filter(Y,M,M))
2:	a__filter(cons(X,Y),s(N),M)	→ cons(mark(X),filter(Y,N,M))
3:	a__sieve(cons(0,Y))	→ cons(0,sieve(Y))
4:	a__sieve(cons(s(N),Y))	→ cons(s(mark(N)),sieve(filter(Y,N,N)))
5:	a__nats(N)	→ cons(mark(N),nats(s(N)))
6:	a__zprimes	→ a__sieve(a__nats(s(s(0))))
7:	mark(filter(X1,X2,X3))	→ a__filter(mark(X1),mark(X2),mark(X3))
8:	mark(sieve(X))	→ a__sieve(mark(X))
9:	mark(nats(X))	→ a__nats(mark(X))
10:	mark(zprimes)	→ a__zprimes
11:	mark(cons(X1,X2))	→ cons(mark(X1),X2)
12:	mark(0)	→ 0
13:	mark(s(X))	→ s(mark(X))
14:	a__filter(X1,X2,X3)	→ filter(X1,X2,X3)
15:	a__sieve(X)	→ sieve(X)
16:	a__nats(X)	→ nats(X)
17:	a__zprimes	→ zprimes

There are 16 dependency pairs:


18:	A__FILTER(cons(X,Y),s(N),M)	→ MARK(X)
19:	A__SIEVE(cons(s(N),Y))	→ MARK(N)
20:	A__NATS(N)	→ MARK(N)
21:	A__ZPRIMES	→ A__SIEVE(a__nats(s(s(0))))
22:	A__ZPRIMES	→ A__NATS(s(s(0)))
23:	MARK(filter(X1,X2,X3))	→ A__FILTER(mark(X1),mark(X2),mark(X3))
24:	MARK(filter(X1,X2,X3))	→ MARK(X1)
25:	MARK(filter(X1,X2,X3))	→ MARK(X2)
26:	MARK(filter(X1,X2,X3))	→ MARK(X3)
27:	MARK(sieve(X))	→ A__SIEVE(mark(X))
28:	MARK(sieve(X))	→ MARK(X)
29:	MARK(nats(X))	→ A__NATS(mark(X))
30:	MARK(nats(X))	→ MARK(X)
31:	MARK(zprimes)	→ A__ZPRIMES
32:	MARK(cons(X1,X2))	→ MARK(X1)
33:	MARK(s(X))	→ MARK(X)

The approximated dependency graph contains one SCC: {18-33}.

Consider the SCC {18-33}. By taking the AF π with π(A__FILTER) = π(a__nats) = π(A__NATS) = π(a__sieve) = π(A__SIEVE) = π(cons) = π(mark) = π(MARK) = π(nats) = π(s) = π(sieve) = 1 together with the lexicographic path order with precedence a__zprimes ≻ A__ZPRIMES ≻ 0, a__filter ≈ filter and a__zprimes ≈ zprimes, the rules in {3-5,7-20,27-30,32,33} are weakly decreasing and the rules in {1,2,6,21-26,31} are strictly decreasing. There is one new SCC.
- Consider the SCC {19,20,27-30,32,33}. By taking the AF π with π(a__nats) = π(A__NATS) = π(a__sieve) = π(A__SIEVE) = π(cons) = π(mark) = π(MARK) = π(nats) = π(sieve) = 1 and π(a__filter) = π(filter) = [1] together with the lexicographic path order with precedence a__filter ≻ 0, a__zprimes ≻ 0, a__zprimes ≻ s, a__filter ≈ filter and a__zprimes ≈ zprimes, the rules in {3-5,7-17,20,27-30,32} are weakly decreasing and the rules in {1,2,6,19,33} are strictly decreasing. There is one new SCC.
  - Consider the SCC {20,28-30,32}. By taking the AF π with π(a__nats) = π(A__NATS) = π(cons) = π(mark) = π(MARK) = π(nats) = π(s) = 1 and π(a__filter) = π(filter) = [1] together with the lexicographic path order with precedence a__filter ≻ 0, a__zprimes ≻ 0, a__zprimes ≻ a__sieve, a__filter ≈ filter, a__sieve ≈ sieve and a__zprimes ≈ zprimes, the rules in {5,7-17,20,29,30,32} are weakly decreasing and the rules in {1-4,6,28} are strictly decreasing. There is one new SCC.
    - Consider the SCC {20,29,30,32}. By taking the AF π with π(A__NATS) = π(a__sieve) = π(cons) = π(mark) = π(MARK) = π(s) = π(sieve) = 1 and π(a__filter) = π(filter) = [1] together with the lexicographic path order with precedence a__filter ≻ 0, a__zprimes ≻ 0, a__zprimes ≻ a__nats, a__filter ≈ filter, a__nats ≈ nats and a__zprimes ≈ zprimes, the rules in {3,4,7-17,20,32} are weakly decreasing and the rules in {1,2,5,6,29,30} are strictly decreasing. There is one new SCC.
      - Consider the SCC {32}. There are no usable rules. By taking the AF π with π(MARK) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 32 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (59.95 seconds) --- May 4, 2006